(*
  Copyright (c) 2009 Barry Schwartz

  Permission is hereby granted, free of charge, to any person
  obtaining a copy of this software and associated documentation
  files (the "Software"), to deal in the Software without
  restriction, including without limitation the rights to use,
  copy, modify, merge, publish, distribute, sublicense, and/or sell
  copies of the Software, and to permit persons to whom the
  Software is furnished to do so, subject to the following
  conditions:

  The above copyright notice and this permission notice shall be
  included in all copies or substantial portions of the Software.

  THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
  EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
  OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
  NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
  HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
  WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
  FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
  OTHER DEALINGS IN THE SOFTWARE.
*)

open XNum
  
exception Inconsistent
  
type var = int

(* index into array *)
type bound = (var * num)

(* (v, n) represents  v + n *)
type equation = var LinForm.lin_form

type coordinate =
  { min : num; max : num; lower_bounds : bound list;
    upper_bounds : bound list; equations : equation list
  }

type system =
  { mutable x_coords : coordinate array; mutable y_coords : coordinate array;
    mutable num_vars : int
  }

let create () = { x_coords = [|  |]; y_coords = [|  |]; num_vars = 0; }
  
let clone system =
  {
    x_coords = Array.copy system.x_coords;
    y_coords = Array.copy system.y_coords;
    num_vars = system.num_vars;
  }
  
let compare_int (x : int) (y : int) =
  if x < y then LinForm.Lt else if x > y then LinForm.Gt else LinForm.Eq
  
let add_variable system min_x min_y max_x max_y =
  let x =
    {
      min = min_x;
      max = max_x;
      lower_bounds = [];
      upper_bounds = [];
      equations = [];
    } in
  let y =
    {
      min = min_y;
      max = max_y;
      lower_bounds = [];
      upper_bounds = [];
      equations = [];
    }
  in
    (if system.num_vars < (Array.length system.x_coords)
     then
       (system.x_coords.(system.num_vars) <- x;
        system.y_coords.(system.num_vars) <- y)
     else
       (system.x_coords <-
          Array.init (2 * system.num_vars)
            (fun i -> if i < system.num_vars then system.x_coords.(i) else x);
        system.y_coords <-
          Array.init (2 * system.num_vars)
            (fun i -> if i < system.num_vars then system.y_coords.(i) else y));
     system.num_vars <- system.num_vars + 1)
  
let update sys =
  let eval_lin_form get_coord lf =
    List.fold_left
      (fun (min, max) (a, x) ->
         if ge_num a num_zero
         then
           ((add_num min (mult_num a (get_coord x).min)),
            (add_num max (mult_num a (get_coord x).max)))
         else
           ((add_num min (mult_num a (get_coord x).max)),
            (add_num max (mult_num a (get_coord x).min))))
      ((lf.LinForm.const), (lf.LinForm.const)) lf.LinForm.terms in
  let update_coord get_coord coord =
    let new_min =
      List.fold_left
        (fun min (var, const) ->
           max_num min (add_num (get_coord var).min const))
        coord.min coord.lower_bounds in
    let new_max =
      List.fold_left
        (fun max (var, const) ->
           min_num max (add_num (get_coord var).max const))
        coord.max coord.upper_bounds in
    let (new_min2, new_max2) =
      List.fold_left
        (fun (min, max) eq ->
           let (l, u) = eval_lin_form get_coord eq
           in ((max_num min l), (min_num max u)))
        (new_min, new_max) coord.equations
    in
      if gt_num new_min2 new_max2
      then raise Inconsistent
      else
        if (gt_num new_min2 coord.min) || (lt_num new_max2 coord.max)
        then Some { (coord) with min = new_min2; max = new_max2; }
        else None in
  let get_x_coord v = sys.x_coords.(v) in
  let get_y_coord v = sys.y_coords.(v) in
  let changed = ref true
  in
    while !changed do changed := false;
      for i = 0 to sys.num_vars - 1 do
        if lt_num sys.x_coords.(i).min sys.x_coords.(i).max
        then
          (match update_coord get_x_coord sys.x_coords.(i) with
           | None -> ()
           | Some c -> (sys.x_coords.(i) <- c; changed := true))
        else ();
        if lt_num sys.y_coords.(i).min sys.y_coords.(i).max
        then
          (match update_coord get_y_coord sys.y_coords.(i) with
           | None -> ()
           | Some c -> (sys.y_coords.(i) <- c; changed := true))
        else ()
      done done
  
let set_x_coord_without_update system var x =
  let old_x = system.x_coords.(var)
  in
    (if (lt_num x old_x.min) || (gt_num x old_x.max)
     then raise Inconsistent
     else ();
     system.x_coords.(var) <-
       { (system.x_coords.(var)) with min = x; max = x; })
  
let set_y_coord_without_update system var y =
  let old_y = system.y_coords.(var)
  in
    (if (lt_num y old_y.min) || (gt_num y old_y.max)
     then raise Inconsistent
     else ();
     system.y_coords.(var) <-
       { (system.y_coords.(var)) with min = y; max = y; })
  
let set_variable system var x y =
  (set_x_coord_without_update system var x;
   set_y_coord_without_update system var y;
   update system)
  
let set_x_coord system var x =
  (set_x_coord_without_update system var x; update system)
  
let set_y_coord system var y =
  (set_y_coord_without_update system var y; update system)
  
let add_equation system add_eq eq =
  match eq.LinForm.terms with
  | [] -> if eq_num eq.LinForm.const num_zero then () else raise Inconsistent
  | _ ->
      let rec iter eq1 eq2 =
        (match eq1.LinForm.terms with
         | [] -> update system
         | (a, v) :: _ ->
             let new_eq1 = LinForm.remove_first_term eq1 in
             let lf =
               LinForm.scale (div_num num_minus_one a)
                 (LinForm.add new_eq1 eq2)
             in
               (add_eq system v lf;
                iter new_eq1 (LinForm.add_unknown eq2 a v)))
      in iter eq (LinForm.of_num compare_int eq.LinForm.const)
  
let add_x_equation system eq =
  let add_x_eq system var eq =
    system.x_coords.(var) <-
      {
        (system.x_coords.(var))
        with
        equations = eq :: system.x_coords.(var).equations;
      }
  in add_equation system add_x_eq eq
  
let add_y_equation system eq =
  let add_y_eq system var eq =
    system.y_coords.(var) <-
      {
        (system.y_coords.(var))
        with
        equations = eq :: system.y_coords.(var).equations;
      }
  in add_equation system add_y_eq eq
  
(* v1 - v2 >= off *)
let add_bound c1 c2 v1 v2 off =
  ({ (c1) with lower_bounds = (v2, off) :: c1.lower_bounds; },
   { (c2) with upper_bounds = (v1, (minus_num off)) :: c2.lower_bounds; })
  
let add_x_bound system v1 v2 off =
  let (c1, c2) =
    add_bound system.x_coords.(v1) system.x_coords.(v2) v1 v2 off
  in (system.x_coords.(v1) <- c1; system.x_coords.(v2) <- c2; update system)
  
let add_y_bound system v1 v2 off =
  let (c1, c2) =
    add_bound system.y_coords.(v1) system.y_coords.(v2) v1 v2 off
  in (system.y_coords.(v1) <- c1; system.y_coords.(v2) <- c2; update system)
  

